ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:ecl(ds; da). ecl-ex(x)  ( List) 

latex

Definitions	, , fpf(A; a.B(a)), x. t(x), Id, ecl-ex(x), ecl ind, x,y,z,w. t(x;y;z;w), x,y. t(x;y), x,y,z. t(x;y;z), [], decl-state(ds), ma-valtype(da; k), Type, Knd, merge(as; bs), if b then t else f fi , type List, ecl(ds; da), left + right, Unit, P  Q, P  Q, x:A  B(x), (i = j), , b, b, prop{i:l}, s = t, s-insert(x; l), x:A. B(x), x:AB(x), , {x:A| B(x)} , A  B, A, False, P  Q, a < b, #$n, t  T
Lemmas	nat plus wf, s-insert wf, assert wf, not wf, bnot wf, bool wf, eq int wf, assert of eq int, not functionality wrt iff, assert of bnot, iff transitivity, eqff to assert, eqtt to assert, ecl wf, nat wf, ifthenelse wf, merge wf, Knd wf, ma-valtype wf, decl-state wf, ecl ind wf, Id wf, fpf wf